| contributor | FMI, Sichere und Zuverlässige Softwaresysteme | ||||||||||||||||
| creator |
Schwoon, Stefan
| Esparza, Javier
| date |
2004-11
| description |
18 pages
|
The automata-theoretic approach to verification of LTL relies on an
algorithm for finding accepting cycles in the product of the system
and a Büchi automaton for the negation of the formula.
Explicit-state model checkers typically construct the product space
"on the fly" and explore the states using depth-first
search. We survey algorithms proposed for this purpose and propose
two improved algorithms, one based on nested DFS, the other on
strongly connected components. We compare these algorithms both
theoretically and experimentally and determine cases where both
algorithms can be useful.
| format |
application/pdf
| 183777 Bytes | |
| identifier | http://www.informatik.uni-stuttgart.de/cgi-bin/NCSTRL/NCSTRL_view.pl?id=TR-2004-06&engl=1 |
| language | eng |
| publisher | Stuttgart, Germany, Universität Stuttgart |
| relation | Technical Report No. 2004/06 |
| source | ftp://ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart_fi/TR-2004-06/TR-2004-06.pdf |
| subject | Software Engineering Software/Program Verification (CR D.2.4) |
| Specifying and Verifying and Reasoning about Programs (CR F.3.1) | |
| Discrete Mathematics Graph Theory (CR G.2.2) | |
| LTL | |
| model checking | |
| depth-first search | |
| title | A Note on On-The-Fly Verification Algorithms |
| type | Text |
| Technical Report |